/-
Copyright (c) 2025 Antoine Chambert-Loir. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Antoine Chambert-Loir
-/
module

public import Mathlib.LinearAlgebra.Determinant
public import Mathlib.LinearAlgebra.Dual.Basis
public import Mathlib.LinearAlgebra.Matrix.Dual
public import Mathlib.LinearAlgebra.GeneralLinearGroup
public import Mathlib.LinearAlgebra.Charpoly.BaseChange

/-!
# The special linear group of a module

If `R` is a commutative ring and `V` is an `R`-module,
we define `SpecialLinearGroup R V` as the subtype of
linear equivalences `V ≃ₗ[R] V` with determinant 1.
When `V` doesn't have a finite basis, the determinant is defined by 1
and the definition gives `V ≃ₗ[R] V`.
The interest of this definition is that `SpecialLinearGroup R V`
has a group structure. (Starting from linear maps wouldn't have worked.)

The file is constructed parallel to the one defining `Matrix.SpecialLinearGroup`.

We provide `SpecialLinearGroup.toLinearEquiv`: the canonical map
from `SpecialLinearGroup R V` to `V ≃ₗ[R] V`, as a monoid hom.

When `V` is free and finite over `R`, we define
* `SpecialLinearGroup.dualMap`
* `SpecialLinearGroup.baseChange`

We define `Matrix.SpecialLinearGroup.toLin'_equiv`: the mul equivalence
from `Matrix.SpecialLinearGroup n R` to `SpecialLinearGroup R (n → R)`
and its variant
`Matrix.SpecialLinearGroup.toLin_equiv`,
from `Matrix.SpecialLinearGroup n R` to `SpecialLinearGroup R V`,
associated with a finite basis of `V`.

-/

@[expose] public section

variable {R V : Type*} [CommRing R] [AddCommGroup V] [Module R V]

variable (R V) in
/-- The special linear group of a module.

This is only meaningful when the module is finite and free,
for otherwise, it coincides with the group of linear equivalences. -/
abbrev SpecialLinearGroup := { u : V ≃ₗ[R] V // u.det = 1 }

namespace SpecialLinearGroup

theorem det_eq_one (u : SpecialLinearGroup R V) :
    LinearMap.det (u : V →ₗ[R] V) = 1 := by
  simp [← LinearEquiv.coe_det, u.prop]

instance : CoeFun (SpecialLinearGroup R V) (fun _ ↦ V → V) where
  coe u x := u.val x

theorem ext_iff (u v : SpecialLinearGroup R V) : u = v ↔ ∀ x : V, u x = v x := by
  simp only [← Subtype.coe_inj, LinearEquiv.ext_iff]

@[ext]
theorem ext (u v : SpecialLinearGroup R V) : (∀ x, u x = v x) → u = v :=
  (SpecialLinearGroup.ext_iff u v).mpr

section rankOne

theorem subsingleton_of_finrank_eq_one [Module.Free R V] (d1 : Module.finrank R V = 1) :
    Subsingleton (SpecialLinearGroup R V) where
  allEq u v := by
    nontriviality R
    ext x
    by_cases hx : x = 0
    · simp [hx]
    suffices ∀ (u : SpecialLinearGroup R V), (u : V →ₗ[R] V) = LinearMap.id by
      simp only [LinearMap.ext_iff, LinearEquiv.coe_coe, LinearMap.id_coe, id_eq] at this
      simp [this u, this v]
    intro u
    ext x
    set c := (LinearEquiv.smul_id_of_finrank_eq_one d1).symm u with hc
    rw [LinearEquiv.eq_symm_apply] at hc
    suffices c = 1 by
      simp [← hc, LinearEquiv.smul_id_of_finrank_eq_one, this]
    have hu := u.prop
    simpa [← Units.val_inj, LinearEquiv.coe_det, ← hc,
      LinearEquiv.smul_id_of_finrank_eq_one, d1] using hu

end rankOne

instance : Inv (SpecialLinearGroup R V) :=
  ⟨fun A => ⟨A⁻¹, by simp [A.prop]⟩⟩

instance : Mul (SpecialLinearGroup R V) :=
  ⟨fun A B => ⟨A * B, by simp [A.prop, B.prop]⟩⟩

instance : Div (SpecialLinearGroup R V) :=
  ⟨fun A B => ⟨A / B, by simp [A.prop, B.prop]⟩⟩

instance : One (SpecialLinearGroup R V) :=
  ⟨⟨1, by simp⟩⟩

instance : Pow (SpecialLinearGroup R V) ℕ where
  pow x n := ⟨x ^ n, by simp [x.prop]⟩

instance : Pow (SpecialLinearGroup R V) ℤ where
  pow x n := ⟨x ^ n, by simp [x.prop]⟩

instance : Inhabited (SpecialLinearGroup R V) :=
  ⟨1⟩

/-- The transpose of an element in `SpecialLinearGroup R V`. -/
def dualMap
    [Module.Free R V] [Module.Finite R V] (A : SpecialLinearGroup R V) :
    SpecialLinearGroup R (Module.Dual R V) :=
  ⟨LinearEquiv.dualMap (A : V ≃ₗ[R] V), by
    simp only [← Units.val_inj, LinearEquiv.coe_det, Units.val_one,
      LinearEquiv.dualMap, LinearMap.det_dualMap]
    simp [← LinearEquiv.coe_det, A.prop]⟩

@[inherit_doc]
scoped postfix:1024 "ᵀ" => SpecialLinearGroup.dualMap

section CoeLemmas

variable (A B : SpecialLinearGroup R V)

theorem coe_mk (A : V ≃ₗ[R] V) (h : A.det = 1) : ↑(⟨A, h⟩ : SpecialLinearGroup R V) = A :=
  rfl

@[simp]
theorem coe_mul : (A * B : SpecialLinearGroup R V) = (A * B  : V ≃ₗ[R] V) :=
  rfl

@[simp]
theorem coe_div : (A / B : SpecialLinearGroup R V) = (A / B  : V ≃ₗ[R] V) :=
  rfl

@[simp]
theorem coe_inv : (A : SpecialLinearGroup R V)⁻¹ = (A⁻¹ : V ≃ₗ[R] V) :=
  rfl

@[simp]
theorem coe_one : (1 : SpecialLinearGroup R V) = (1 : V ≃ₗ[R] V) :=
  rfl

@[simp]
theorem det_coe : LinearEquiv.det (A : V ≃ₗ[R] V) = 1 :=
  A.prop

@[simp]
theorem coe_pow (m : ℕ) : (A ^ m : SpecialLinearGroup R V) = (A : V ≃ₗ[R] V) ^ m :=
  rfl

@[simp]
theorem coe_zpow (m : ℤ) : (A ^ m : SpecialLinearGroup R V) = (A : V ≃ₗ[R] V) ^ m :=
  rfl

@[simp]
theorem coe_dualMap
    [Module.Free R V] [Module.Finite R V] :
    Aᵀ = (A : V ≃ₗ[R] V).dualMap :=
  rfl

end CoeLemmas

instance : Group (SpecialLinearGroup R V) := fast_instance%
  Function.Injective.group _ Subtype.coe_injective coe_one coe_mul coe_inv coe_div coe_pow coe_zpow

/-- A version of `Matrix.toLin' A` that produces linear equivalences. -/
def toLinearEquiv : SpecialLinearGroup R V →* V ≃ₗ[R] V where
  toFun A := A.val
  map_one' := coe_one
  map_mul' := coe_mul

theorem toLinearEquiv_apply (A : SpecialLinearGroup R V) (v : V) :
    A.toLinearEquiv v = A v :=
  rfl

theorem toLinearEquiv_to_linearMap (A : SpecialLinearGroup R V) :
    (SpecialLinearGroup.toLinearEquiv A) = (A : V →ₗ[R] V) :=
  rfl

theorem toLinearEquiv_symm_apply (A : SpecialLinearGroup R V) (v : V) :
    A.toLinearEquiv.symm v = A⁻¹ v :=
  rfl

theorem toLinearEquiv_symm_to_linearMap (A : SpecialLinearGroup R V) :
    A.toLinearEquiv.symm = ((A⁻¹ : SpecialLinearGroup R V) : V →ₗ[R] V) :=
  rfl

theorem toLinearEquiv_injective :
    Function.Injective (toLinearEquiv : SpecialLinearGroup R V →* V ≃ₗ[R] V) :=
  Subtype.val_injective

/-- The canonical group morphism from the special linear group
to the general linear group. -/
def toGeneralLinearGroup : SpecialLinearGroup R V →* LinearMap.GeneralLinearGroup R V :=
  (LinearMap.GeneralLinearGroup.generalLinearEquiv R V).symm.toMonoidHom.comp toLinearEquiv

lemma toGeneralLinearGroup_toLinearEquiv_apply (u : SpecialLinearGroup R V) :
    u.toGeneralLinearGroup.toLinearEquiv = u.toLinearEquiv := rfl

lemma coe_toGeneralLinearGroup_apply (u : SpecialLinearGroup R V) :
    u.toGeneralLinearGroup.val = u.toLinearEquiv := rfl

lemma toGeneralLinearGroup_injective :
    Function.Injective ⇑(toGeneralLinearGroup (R := R) (V := V)) :=  by
  simp [toGeneralLinearGroup, toLinearEquiv_injective]

lemma mem_range_toGeneralLinearGroup_iff {u : LinearMap.GeneralLinearGroup R V} :
    u ∈ Set.range ⇑(toGeneralLinearGroup (R := R) (V := V)) ↔
      u.toLinearEquiv.det = 1 := by
  constructor
  · rintro ⟨v, hv⟩
    rw [← hv, toGeneralLinearGroup_toLinearEquiv_apply]
    exact v.prop
  · intro hu
    refine ⟨⟨u.toLinearEquiv, hu⟩, rfl⟩

section baseChange

open TensorProduct

variable {S : Type*} [CommRing S] [Algebra R S]
  [Module.Free R V] [Module.Finite R V]

/-- By base change, an `R`-algebra `S` induces a group homomorphism from
`SpecialLinearGroup R V` to `SpecialLinearGroup S (S ⊗[R] V)`. -/
@[simps]
def baseChange : SpecialLinearGroup R V →* SpecialLinearGroup S (S ⊗[R] V) where
  toFun g := ⟨LinearEquiv.baseChange R S V V g, by
      rw [LinearEquiv.det_baseChange, g.prop, map_one]⟩
  map_one' := Subtype.ext <| by simp
  map_mul' x y := Subtype.ext <| by simp [LinearEquiv.baseChange_mul]

end baseChange

variable {W X : Type*} [AddCommGroup W] [Module R W] [AddCommGroup X] [Module R X]

/-- The isomorphism between special linear groups of isomorphic modules. -/
def congr_linearEquiv (e : V ≃ₗ[R] W) :
    SpecialLinearGroup R V ≃* SpecialLinearGroup R W where
  toFun f := ⟨e.symm ≪≫ₗ f ≪≫ₗ e, by simp [f.prop]⟩
  invFun g := ⟨e ≪≫ₗ g ≪≫ₗ e.symm, by
    nth_rewrite 1 [← LinearEquiv.symm_symm e]
    rw [LinearEquiv.det_conj g e.symm, g.prop]⟩
  left_inv f := Subtype.coe_injective <| by aesop
  right_inv g := Subtype.coe_injective <| by aesop
  map_mul' f g := Subtype.coe_injective <| by aesop

@[simp]
theorem congr_linearEquiv_coe_apply (e : V ≃ₗ[R] W) (f : SpecialLinearGroup R V) :
    (congr_linearEquiv e f : W ≃ₗ[R] W) = e.symm ≪≫ₗ f ≪≫ₗ e :=
  rfl

@[simp]
theorem congr_linearEquiv_apply_apply (e : V ≃ₗ[R] W) (f : SpecialLinearGroup R V) (x : W) :
    congr_linearEquiv e f x = e (f (e.symm x)) :=
  rfl

theorem congr_linearEquiv_symm (e : V ≃ₗ[R] W) :
    (congr_linearEquiv e).symm = congr_linearEquiv e.symm :=
  rfl

theorem congr_linearEquiv_trans (e : V ≃ₗ[R] W) (f : W ≃ₗ[R] X) :
    (congr_linearEquiv e).trans (congr_linearEquiv f) = congr_linearEquiv (e.trans f) := by
  rfl

theorem congr_linearEquiv_refl :
    congr_linearEquiv (LinearEquiv.refl R V) = MulEquiv.refl _ := by
  rfl

end SpecialLinearGroup

namespace Matrix.SpecialLinearGroup

variable {n : Type*} [Fintype n] [DecidableEq n] (b : Module.Basis n R V)

/-- The canonical isomorphism from `SL(n, R)` to the special linear group of the module `n → R`. -/
def toLin'_equiv : SpecialLinearGroup n R ≃* _root_.SpecialLinearGroup R (n → R) where
  toFun A := ⟨Matrix.SpecialLinearGroup.toLin' A,
    by
      simp [← Units.val_inj, LinearEquiv.coe_det, Units.val_one,
        Matrix.SpecialLinearGroup.toLin'_to_linearMap]⟩
  invFun u := ⟨LinearMap.toMatrix' u,
      by simp [← LinearEquiv.coe_det, u.prop]⟩
  left_inv A := Subtype.coe_injective <| by
    rw [← LinearEquiv.eq_symm_apply, LinearMap.toMatrix'_symm,
      Matrix.SpecialLinearGroup.toLin'_to_linearMap]
  right_inv u := Subtype.coe_injective <| by
    simp [← LinearEquiv.toLinearMap_inj, Matrix.SpecialLinearGroup.toLin']
  map_mul' A B := Subtype.coe_injective (by simp)

/-- The isomorphism from `Matrix.SpecialLinearGroup n R`
to the special linear group of a module associated with a basis of that module. -/
noncomputable def toLin_equiv (b : Module.Basis n R V) :
    SpecialLinearGroup n R ≃* _root_.SpecialLinearGroup R V :=
  SpecialLinearGroup.toLin'_equiv.trans
    (SpecialLinearGroup.congr_linearEquiv b.equivFun.symm)

theorem toLin_equiv.toLinearMap_eq
    (b : Module.Basis n R V) (g : Matrix.SpecialLinearGroup n R) :
    (toLin_equiv b g : V →ₗ[R] V) = (Matrix.toLin b b g) :=
  rfl

theorem toLin_equiv.symm_toLinearMap_eq
    (b : Module.Basis n R V) (g : _root_.SpecialLinearGroup R V) :
    ((toLin_equiv b).symm g : Matrix n n R) = LinearMap.toMatrix b b g :=
  rfl

end Matrix.SpecialLinearGroup

namespace SpecialLinearGroup

section center

variable [Module.Free R V] [Module.Finite R V]

theorem center_eq_bot_of_finrank_le_one (h : Module.finrank R V ≤ 1) :
    Subgroup.center (SpecialLinearGroup R V) = ⊥ := by
  nontriviality R
  let b := Module.Free.chooseBasis R V
  have : Subsingleton (Module.Free.ChooseBasisIndex R V) := by
    rwa [← Finite.card_le_one_iff_subsingleton,
      Nat.card_eq_fintype_card, ← Module.finrank_eq_card_basis b]
  have : Subsingleton (Subgroup.center
    (Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)) := by
    infer_instance
  rw [Equiv.subsingleton_congr
    (Subgroup.centerCongr (Matrix.SpecialLinearGroup.toLin_equiv b)).toEquiv] at this
  exact Subgroup.eq_bot_of_subsingleton _

theorem mem_center_iff {g : SpecialLinearGroup R V} :
    g ∈ Subgroup.center (SpecialLinearGroup R V) ↔
      ∃ (r : R), r ^ (Module.finrank R V) = 1 ∧
        (g : V →ₗ[R] V) = r • LinearMap.id := by
  rcases subsingleton_or_nontrivial R with hR | hR
  · have : Subsingleton (SpecialLinearGroup R V) := inferInstance
    simp [Subsingleton.eq_one g]
  let b := Module.Free.chooseBasis R V
  let := Module.Free.ChooseBasisIndex.fintype R V
  rw [Module.finrank_eq_card_basis b]
  let e := (Matrix.SpecialLinearGroup.toLin_equiv b).symm
  rw [← show e g ∈ Subgroup.center _ ↔ g ∈ Subgroup.center _ from
    MulEquivClass.apply_mem_center_iff e]
  rw [Matrix.SpecialLinearGroup.mem_center_iff]
  apply exists_congr
  simp only [Matrix.scalar_apply, and_congr_right_iff, e]
  intro r hr
  suffices ((Matrix.SpecialLinearGroup.toLin_equiv b).symm g) =
    Matrix.of fun i j ↦ (b.repr (g (b j))) i by
    simp only [this]
    rw [← (LinearMap.toMatrix b b).injective.eq_iff]
    simp only [← Matrix.ext_iff, Matrix.of_apply]
    apply forall₂_congr
    intro i j
    simp [Matrix.diagonal, LinearMap.toMatrix_apply,
      Finsupp.single, Pi.single_apply, Iff.symm eq_comm]
  ext
  simp [Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, LinearMap.toMatrix_apply]

theorem mem_center_iff_spec {g : SpecialLinearGroup R V}
    (hg : g ∈ Subgroup.center (SpecialLinearGroup R V)) (x : V) :
    (g : V →ₗ[R] V) x = (mem_center_iff.mp hg).choose • x := by
  let H := (mem_center_iff.mp hg).choose_spec.2
  rw [LinearMap.ext_iff] at H
  simp [H]

/- TODO : delete this auxiliary definition
and put it in the definition of `centerEquivRootsOfUnity.
How can one access to the definition of one already defined term in a structure
while one is still definining it? -/
/-- The inverse map for the equivalence `SpecialLinearGroup.centerEquivRootsOfUnity`. -/
noncomputable def centerEquivRootsOfUnity_invFun
    (r : rootsOfUnity (max (Module.finrank R V) 1) R) :
    Subgroup.center (SpecialLinearGroup R V) :=
  ⟨⟨LinearMap.equivOfIsUnitDet (M := V) (R := R) (f := ((r : Rˣ) : R) • LinearMap.id) (by
    simp [LinearMap.det_smul, IsUnit.pow]), by
    simp only [← Units.val_inj, LinearEquiv.coe_det, LinearMap.coe_equivOfIsUnitDet,
      LinearMap.det_smul, LinearMap.det_id, mul_one, Units.val_one]
    have := (mem_rootsOfUnity' _ _).mp r.prop
    rcases max_cases (Module.finrank R V) 1 with ⟨h, h'⟩ |  ⟨h, h'⟩
    · simp_rw [h] at this
      exact this
    · simp_rw [h, pow_one] at this
      simp [this]⟩, by
    simp only [mem_center_iff, LinearMap.coe_equivOfIsUnitDet]
    use r.val
    simp only [and_true]
    let ⟨r, hr⟩ := r
    by_cases hV : Module.finrank R V = 0
    · simp [hV]
    · rw [← ne_eq, ← Nat.one_le_iff_ne_zero] at hV
      rw [mem_rootsOfUnity', max_eq_left hV] at hr
      simpa [← Subtype.val_inj, ← Units.val_inj]⟩

open Classical in
/-- The isomorphism between the roots of unity and the center of the special linear group. -/
noncomputable def centerEquivRootsOfUnity :
    (Subgroup.center (SpecialLinearGroup R V)) ≃*
      ↥(rootsOfUnity (max (Module.finrank R V) 1) R) where
  toFun g := (subsingleton_or_nontrivial R).by_cases
    (fun _ ↦ 1)
    (fun hR ↦ (subsingleton_or_nontrivial V).by_cases
      (fun _ ↦ 1)
      (fun hV ↦ by
        rw [← Module.finrank_pos_iff_of_free (R := R)] at hV
        replace hV : 1 ≤ Module.finrank R V := hV
        have hr := (mem_center_iff.mp g.prop).choose_spec.1
        set r := (mem_center_iff.mp g.prop).choose
        rw [← Nat.max_eq_left hV] at hr
        have : IsUnit r := by
          rw [← isUnit_pow_iff _, hr]
          · exact isUnit_one
          rw [Nat.max_eq_left hV]
          exact Nat.ne_zero_of_lt hV
        exact ⟨this.unit, by simp [mem_rootsOfUnity, ← Units.val_inj, hr]⟩))
  invFun := centerEquivRootsOfUnity_invFun
  left_inv g := by
    simp only [centerEquivRootsOfUnity_invFun, ← Subtype.val_inj,
      ← LinearEquiv.toLinearMap_inj, LinearMap.coe_equivOfIsUnitDet]
    simp only [Or.by_cases]
    split_ifs with hR hV
    · simp [Subsingleton.eq_one g]
    · simp [Subsingleton.eq_one g]
    · simp only [IsUnit.unit_spec, ← (mem_center_iff.mp g.prop).choose_spec.2]
  right_inv r := by
    rw [← Subtype.val_inj, SetLike.coe_eq_coe]
    simp only [Or.by_cases]
    split_ifs with hR hV
    · simp [Subsingleton.eq_one r]
    · replace hR := not_subsingleton_iff_nontrivial.mp hR
      symm
      rw [← Module.finrank_eq_zero_iff_of_free (R := R)] at hV
      simpa [hV] using (mem_rootsOfUnity _ _).mp r.prop
    · rw [not_subsingleton_iff_nontrivial] at hV
      have := Module.Free.instFaithfulSMulOfNontrivial R V
      simp only [← Subtype.val_inj, ← Units.val_inj, IsUnit.unit_spec]
      have H := mem_center_iff.mp (Subtype.prop (centerEquivRootsOfUnity_invFun r))
      suffices (H.choose • LinearMap.id : V →ₗ[R] V) = (r.val : R) • LinearMap.id by
        apply FaithfulSMul.eq_of_smul_eq_smul (α := V)
        intro x
        rw [LinearMap.ext_iff] at this
        simp only [LinearMap.smul_apply, LinearMap.id_coe, id_eq] at this
        rw [this x]
      rw [← H.choose_spec.2]
      simp [centerEquivRootsOfUnity_invFun]
  map_mul' g h := by
    simp only [Or.by_cases, Subgroup.coe_mul, coe_mul, LinearEquiv.coe_toLinearMap_mul,
      mul_dite, mul_one, dite_mul, one_mul, MulMemClass.mk_mul_mk]
    split_ifs with hR hV
    · rfl
    · rfl
    rw [not_subsingleton_iff_nontrivial] at hV
    have := Module.Free.instFaithfulSMulOfNontrivial R V
    set Hg := (mem_center_iff.mp g.prop)
    set Hh := (mem_center_iff.mp h.prop)
    set Hgh := (mem_center_iff.mp (g * h).prop)
    simp only [← Subtype.val_inj, ← Units.val_inj, IsUnit.unit_spec,
      Units.val_mul]
    change Hgh.choose = Hg.choose * Hh.choose
    suffices (Hgh.choose • LinearMap.id : V →ₗ[R] V)
      = (Hg.choose • LinearMap.id) * (Hh.choose • LinearMap.id) by
      apply FaithfulSMul.eq_of_smul_eq_smul (α := V)
      intro x
      simp  [mul_smul,
        ← mem_center_iff_spec (g * h).prop, ← mem_center_iff_spec h.prop,
        ← mem_center_iff_spec g.prop]
    simp [← Hgh.choose_spec.2, ← Hh.choose_spec.2, ← Hg.choose_spec.2]

theorem centerEquivRootsOfUnity_apply
    (g : Subgroup.center (SpecialLinearGroup R V)) :
    (g : V →ₗ[R] V) = (centerEquivRootsOfUnity g) • LinearMap.id := by
  simp only [centerEquivRootsOfUnity, Or.by_cases, MulEquiv.coe_mk, Equiv.coe_fn_mk,
    dite_smul, one_smul, Subgroup.mk_smul, Units.smul_isUnit, dite_eq_ite]
  split_ifs with hR hV
  · have : Subsingleton V := Module.subsingleton R V
    apply Subsingleton.eq_one
  · apply Subsingleton.eq_one
  · rw [not_subsingleton_iff_nontrivial] at hV
    rw [← (mem_center_iff.mp g.prop).choose_spec.2]

theorem centerEquivRootsOfUnity_apply_apply
    (g : Subgroup.center (SpecialLinearGroup R V)) (x : V) :
    (centerEquivRootsOfUnity g) • x = (g : SpecialLinearGroup R V) x := by
  simp only
  rw [← LinearEquiv.coe_toLinearMap, centerEquivRootsOfUnity_apply]
  simp

theorem _root_.rootsOfUnity.eq_one {n : ℕ} {r : rootsOfUnity n R}
    (hn : n = 1) : r.val = 1 := by
  have h := r.prop
  simpa only [mem_rootsOfUnity, hn, pow_one] using h

theorem centerEquivRootsOfUnity_apply_of_finrank_le_one
    (d1 : Module.finrank R V ≤ 1) (g : Subgroup.center (SpecialLinearGroup R V)) :
    centerEquivRootsOfUnity g = 1 := by
  rw [← Subtype.coe_inj, OneMemClass.coe_one]
  apply rootsOfUnity.eq_one
  rw [Nat.max_eq_right d1]

theorem centerEquivRootsOfUnity_symm_apply
    (r : rootsOfUnity (max (Module.finrank R V) 1) R) :
    (centerEquivRootsOfUnity.symm r : V →ₗ[R] V) = r • LinearMap.id := by
  simp only [centerEquivRootsOfUnity, MulEquiv.symm_mk, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk,
    centerEquivRootsOfUnity_invFun, LinearMap.coe_equivOfIsUnitDet]
  congr

section

open Subgroup Matrix Matrix.SpecialLinearGroup

variable {n : Type*} [Fintype n] [DecidableEq n] {R : Type*} [CommRing R]

-- variable [Nontrivial R]
variable {V : Type*} [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V]
variable {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R V)

-- compare with `Matrix.SpecialLinearGroup.centerEquivRootsOfUnity`
-- TODO : golf!
theorem centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq (g) :
    ((centerCongr (toLin_equiv b)).trans centerEquivRootsOfUnity g).val =
      Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity g := by
  nontriviality R
  by_cases hV : Subsingleton V
  · convert Eq.refl (1 : Rˣ) <;>
    · apply rootsOfUnity.eq_one
      rw [← Module.finrank_eq_zero_iff_of_free (R := R)] at hV
      simp only [hV, sup_eq_right, zero_le_one, ← Module.finrank_eq_card_basis b]
  · have hι : ¬ IsEmpty ι := fun hι ↦ hV (by
      rw [← Module.finrank_eq_zero_iff_of_free (R := R),
        Module.finrank_eq_card_basis b, Fintype.card_of_isEmpty])
    rw [not_subsingleton_iff_nontrivial] at hV
    have := Module.Free.instFaithfulSMulOfNontrivial R V
    suffices (((((Subgroup.centerCongr (Matrix.SpecialLinearGroup.toLin_equiv b)).trans
      centerEquivRootsOfUnity g).val : R) • LinearMap.id) : V →ₗ[R] V) =
        ((Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity g).val : R) • LinearMap.id by
      rw [← Units.val_inj]
      apply FaithfulSMul.eq_of_smul_eq_smul (α := V)
      intro x
      simp only [MulEquiv.trans_apply, LinearMap.ext_iff, LinearMap.smul_apply, LinearMap.id_coe,
        id_eq] at this
      rw [MulEquiv.trans_apply, this]
    simp only [MulEquiv.trans_apply]
    have hgg' := Subgroup.centerCongr_apply_coe (Matrix.SpecialLinearGroup.toLin_equiv b) g
    rw [← Subtype.coe_inj, ← LinearEquiv.toLinearMap_inj, LinearMap.ext_iff] at hgg'
    set g' := ((Subgroup.centerCongr (Matrix.SpecialLinearGroup.toLin_equiv b)) g)
    ext x
    have := centerEquivRootsOfUnity_apply_apply g' x
    simp only [smul_def, Units.smul_def] at this
    simp only [LinearMap.smul_apply, LinearMap.id_coe, id_eq]
    rw [this, ← LinearEquiv.coe_toLinearMap, hgg',
      Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq,
      Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity g,
      Matrix.toLin_scalar]
    simp

end

end center

end SpecialLinearGroup
